$\forall$$T$:Type, $x$:$T$, $l_{1}$,$l_{2}$:($T$ List). ($x$ $\in$ append($l_{1}$; $l_{2}$)) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ $l_{1}$) $\vee$ ($x$ $\in$ $l_{2}$))